-------------------------------------------------------------------------------

const

  ------    common part    ------
  DataCnt: 2;

  ------ outside a cluster ------
  HomeCnt: 1;
  RmtCnt:  2;
  ProcCnt: HomeCnt+RmtCnt;

  ------ inside a cluster  ------
  
  NODE_NUM :  2;

-------------------------------------------------------------------------------

type

  ------    common part    ------
  ClusterCnt:   0..ProcCnt; 
  NODE :   scalarset(NODE_NUM);
  Datas :  scalarset(DataCnt);
  L2Name:  enum{L2};
  NODE_L2: union {NODE, L2Name};

  Homes: enum {Home};
  Rmt: scalarset(RmtCnt);
  Procss: union {Homes, Rmt};

  CacheCnt: 0..NODE_NUM;
  RACState: enum {
        Inval,   -- Invalid
        WRD,     -- basic operation -- waiting for a read reply
        WRDO,    -- basic operation -- waiting for a read reply
                                    -- with ownership transfer
        WRDX,    -- basic operation -- waiting for a read exclusive reply
        WINV,    -- basic operation -- waiting for invalidate acknowledges
        RRD      -- basic operation -- invalidated read/read
    };

  CACHE_STATE : enum {CACHE_I, CACHE_S, CACHE_E, CACHE_M};
  L2State:      enum{Invld, Shrd, Excl};
  NODE_CMD :    enum {NODE_None, NODE_Get, NODE_GetX};

  NODE_STATE: record
      ProcCmd :   NODE_CMD;
      InvMarked : boolean;
      CacheState: CACHE_STATE;
      CacheData : Datas;

      block_WB: boolean;
    end;

  -- uni msg channel
  UNI_CMD: enum {UNI_None, UNI_Get, UNI_GetX, UNI_Put, UNI_PutX, UNI_Nak, UNI_PutXX,
		 WB_WbAck};
  UNI_MSG: record
    Cmd: UNI_CMD;
    Proc: NODE_L2;
    Data: Datas;
  end;

  -- invalidation msg channel
  INV_CMD: enum {INV_None, INV_Inv, INV_InvAck};
  INV_MSG: record
    Cmd: INV_CMD;
  end;

  -- writeback msg channel
  WB_CMD: enum {WB_None, WB_Wb};
  WB_MSG: record
    Cmd: WB_CMD;
    Proc: NODE_L2;
    Data: Datas;
  end;

  -- ShWb msg channel
  SHWB_CMD: enum {SHWB_None, SHWB_ShWb, SHWB_FAck};
  SHWB_MSG: record
    Cmd: SHWB_CMD;
    Proc: NODE_L2;
    Data: Datas;
    Aux: NODE_L2;
  end;

  -- nack-home msg channel
  NAKC_CMD: enum {NAKC_None, NAKC_Nakc,
                  NAKC_SD};
  NAKC_MSG: record
    Cmd: NAKC_CMD;
    Proc: NODE_L2;
    Aux: NODE_L2;
  end;

  GUNI_CMD: enum {GUNI_None, RD_H, RD_RAC, RDX_H, RDX_RAC, ACK, NAK, NAK_Home,
		IACK, IACKX, WB_Ack};

GINV_CMD: enum {GINV_None, INV, SACK};
GINV_MSG: record
  Cmd: GINV_CMD;
  Cluster: Procss;
end;

GWB_CMD: enum {GWB_None, WB};
GWB_MSG: record
  Cmd: GWB_CMD;
  Cluster: Procss;
  Data: Datas;
end;

GSHWB_CMD: enum {GSHWB_None, SHWB, DXFER};
GSHWB_MSG: record
  Cmd: GSHWB_CMD;
  Cluster: Procss;
  Data: Datas;
end;

GNAKC_CMD: enum {GNAKC_None, GNAKC_Nakc, GNAKC_DIR};
GNAKC_MSG: record
  Cmd: GNAKC_CMD;
  Cluster: Procss;
end;



  -- Feb 14
  inClusterReqType: enum {sNone, 
			  sGet,    -- simple Get 
			  sGetX    -- simple GetX
                          };

  -- Feb 14
  inClusterRequest: record
    -- src: NODE;
    reqType: inClusterReqType; 
  end;
  -- Feb 14
  outClusterReply: record
    cmd: GUNI_CMD;
    data: Datas;
  end;
  -- Feb 14
  outClusterRequest: record
    src: Procss;
    reqType: inClusterReqType;
  end;

  -- main structure
  ProcState: record

  /*
    -- these 3 are for invariant purposes
    CurrData: Datas;  
    PrevData: Datas;
    Collecting: boolean;

    -- structure inside a cluster 
    Proc :   array [NODE] of NODE_STATE;

    UniMsg: array [NODE_L2] of UNI_MSG;
    InvMsg: array [NODE_L2] of INV_MSG;
    WbMsg: WB_MSG;
    ShWbMsg: SHWB_MSG;
    NakcMsg: NAKC_MSG;
  */

    -- Feb 14
    inRequest: inClusterRequest;  -- inside cluster sent to outside
    ifInReq: boolean;  -- if the cluster requests to global dir
    -- Feb 14
    ifOutReply: boolean; -- if a reply is received from outside
    outReply: outClusterReply;  -- outside reply to this cluster
    -- Feb 14
    inReply: outClusterReply;
    ifInReply: boolean; -- if this cluster is replying request coming from outside
    -- Feb 14
    outRequest: outClusterRequest; -- request coming from outside
    ifOutReq: boolean;  -- if this cluster receives a request from outside
    -- Feb 14
    outInvReq: GINV_MSG;
    ifOutInv: boolean;
    -- Feb 14
    ifInvReply: boolean;
    invReply: GINV_MSG;
    -- 
    ifWBReq: boolean;
    WBReq: GWB_MSG;
    -- Mar 31
    -- ifGWB_Ack: boolean;


    -- local dir
    L2: record

    /*
      pending: boolean;  
      ShrSet:  array [NODE] of boolean; 
      InvCnt: CacheCnt;
      HeadPtr: NODE_L2; 
    */
      State:   L2State;
      Data:    Datas;
      Dirty:   boolean;
      OnlyCopy: boolean; -- if this cluster has the only copy
      Gblock_WB: boolean;
      -- abstracted May 2
      -- isRetired: boolean;   -- used when a requestX coming from a cluster, 
               	            -- and the cluster is shared with OnlyCopy = false,
	                    -- so when InvCnt = 0 inside the cluster, 
     	                    -- pending cannot always be reset at this time,
                            -- it may need to wait for the outside reply to come back
    end;

    -- communicating with outside cluster
    RAC: record
      State:   RACState;
      InvCnt:  ClusterCnt;
    end;
  end;


  ------ outside a cluster  ------

  DirState: record
    isBusy: boolean;
    Mem: Datas;
    State: L2State;
    ShrSet: array [Procss] of boolean;
    isLocal: boolean;
    HeadPtr: Procss;
  end;


GUNI_MSG: record
  Cmd: GUNI_CMD;
  Cluster: Procss;
  InvCnt: ClusterCnt;
  Data: Datas;
end;


-------------------------------------------------------------------------------

var

  titi: array[Procss] of 1..10;
  toto: array[Procss] of array[Procss] of 1..10;
  tutu: record
      tab: array[Procss] of 1..10;
      i : 1..10;
      tab2: array[Procss] of array[Procss] of 1..10;
  end;
  tata : array[Procss] of record
     i : 1..10;
     j : 1..10;
     tab : array[Procss] of record
        k : 1..10;
        l : 1..10;
     end;
  end;

  GUniMsg: array [Procss] of GUNI_MSG;
  GInvMsg: array [Procss] of GINV_MSG;
  GWbMsg:  GWB_MSG;
  GShWbMsg: GSHWB_MSG;
  GNakcMsg: GNAKC_MSG;

  Procs: array [Procss] of ProcState;
  Dir: DirState;
  SysData: Datas;

-------------------------------------------------------------------------------


-- initializer
ruleset d: Datas do
startstate "Init"

  for p: Procss do
    undefine GUniMsg[p];
    undefine GInvMsg[p];
    GUniMsg[p].Cmd := GUNI_None;
    GInvMsg[p].Cmd := GINV_None;
  end;
  GWbMsg.Cmd := GWB_None;
  GShWbMsg.Cmd := GSHWB_None;
  GNakcMsg.Cmd := GNAKC_None;


  for p: Procss do
    undefine Procs[p];

    Procs[p].L2.State := Invld;
    Procs[p].L2.Dirty := false;
    Procs[p].L2.OnlyCopy := false;
    Procs[p].L2.Gblock_WB := false;
    Procs[p].RAC.State := Inval;
    Procs[p].RAC.InvCnt := 0;
    Procs[p].ifInReq := false;
    Procs[p].ifOutReply := false;
    Procs[p].ifInReply := false;
    Procs[p].ifOutReq := false;
    Procs[p].ifOutInv := false;
    Procs[p].ifInvReply := false;
    Procs[p].ifWBReq := false;

  end;

  undefine Dir;
  Dir.isBusy := false;
  Dir.Mem := d;
  Dir.State := Invld;
  Dir.isLocal := false;
  for p: Rmt do
    Dir.ShrSet[p] := false;
  end;

  SysData := d;
endstartstate;
endruleset;

